$\forall$$A$, $C$:Type, ${\it eqa}$:EqDecider($A$), ${\it eqc}$:EqDecider($C$), ${\it eqc'}$:Top, $r$:($A$$\rightarrow$$C$), $f$:$a$:$A$ fp$\rightarrow$ Top, $a$:$A$.
\\[0ex]\{($\uparrow$$a$ $\in$ dom($f$)) $\Rightarrow$ ($\uparrow$$r$($a$) $\in$ dom(rename($r$;$f$)))\}